T:Type{i}, L:T List, R:({x:T| (x  L) }es_realizer{i:l}), P:({x:T| (x  L) }ES{i}Prop{i'}).
(xL. R(x) ||-{i} es.P(x,es))
 (xL. yL. R-compat{i:l}(R(x); R(y))  x = y  T)
 xL.R(x) ||-{i} es.xL. P(x,es) 

latex

Definitions	xL. P(x), R ||- es.P(es), P  Q, left+right, A || B, s = t, Prop, Realizer, type List, Type, x:AB(x), x:AB(x), R-Feasible(R), x(s1,s2), xL.R(x), x. t(x), {x:A| B(x) }, (x  l), ES, P & Q, P  Q, t  T, x:A. B(x), Consistent(R;es), x(s), f(a), x.A(x), P  Q
Lemmas	R-consistent-Rall, R-feasible-Rall, event system wf, l member wf, Rall wf, R-consistent wf, es realizer wf, R-Feasible wf, R-compat wf